Nuprl Lemma : ma-outlinks_wf
0,22
postcript
pdf
M
:MsgA,
i
:Id. ma-outlinks(
M
;
i
)
(IdLnk
Id
Type) List
latex
Definitions
IdLnk
,
Id
,
MsgA
,
Valtype(
da
;
k
)
,
ma-outlinks(
M
;
i
)
,
da-outlinks(
da
;
i
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
da-outlinks
wf
,
msga
wf
,
Id
wf
origin
M:MsgA, i:Id. ma-outlinks(M;i) 
(IdLnk
IdType) List M:MsgA, i:Id. ma-outlinks(M;i) (IdLnkIdType) List x:A. B(x) T